Nuprl Definition : rng_one 13,42
1 == (r.2.2.2.2.2.2.2).1 
latex

clarification:

1r == (r.2.2.2.2.2.2.2).1 
latex

Uprng sig object directory
Wellformedness Lemmasrng one wf
Definitionst.1, t.2

origin